#pragma once
#include "PDTExpBoolUn.h"
#include "PDTBoolConst.h"

class PDTNot  :  public PDTExpBoolUn, public TraverseIfc <PDTNot , PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTNot )
public:

  PDTNot(PDTCodeGraph & CG, PDTExpBool &operand);

  NodeTypeEnum
  getType()
  {
    return PDTNot_Em;
  }

  PDTExpBool * getExpression() {
      return dynamic_cast<PDTExpBool*>(children[0]);
  }

  virtual void
  printType()
  {
    cout << "PDTNot_Em";
  }

  bool
  isNot()
  {
    return true;
  }

  virtual bool eval(PDTCodeGraph &CG)
  {
	  children[0]->eval(CG);
	  PDTBoolConst* child = dynamic_cast<PDTBoolConst*>(children[0]->getNValue());
	  int result = !child->getValue();
	  nValue = new PDTBoolConst(CG, result);
	  cout<<"Inversion Result of "<<child->getValue()<<": "<<result<<endl;
	  return true;
  }

  virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpBool* childClone = (PDTExpBool*)(children[0]->clone(CG));
		toReturn = new PDTNot(CG, *childClone);
		return toReturn;
	}

  virtual stringstream &
  toString(stringstream & ss) const
  {
    ss << "Not ( ";
    children[0]->toString(ss) << " )";
    return ss;
  }

  virtual Z3_ast
  Z3NodeVisit (PDTZ3Visitor &ZV);
};

